active proctype sat() {
	bool p0, p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p20, p21, p22, p23, p24, p25, p26, p27, p28, p29, p30, p31, p32, p33, p34, p35;
	bool result;

	if :: p0 = true :: p0 = false fi;
	if :: p1 = true :: p1 = false fi;
	if :: p2 = true :: p2 = false fi;
	if :: p3 = true :: p3 = false fi;
	if :: p4 = true :: p4 = false fi;
	if :: p5 = true :: p5 = false fi;
	if :: p6 = true :: p6 = false fi;
	if :: p7 = true :: p7 = false fi;
	if :: p8 = true :: p8 = false fi;
	if :: p9 = true :: p9 = false fi;
	if :: p10 = true :: p10 = false fi;
	if :: p11 = true :: p11 = false fi;
	if :: p12 = true :: p12 = false fi;
	if :: p13 = true :: p13 = false fi;
	if :: p14 = true :: p14 = false fi;
	if :: p15 = true :: p15 = false fi;
	if :: p16 = true :: p16 = false fi;
	if :: p17 = true :: p17 = false fi;
	if :: p18 = true :: p18 = false fi;
	if :: p19 = true :: p19 = false fi;
	if :: p20 = true :: p20 = false fi;
	if :: p21 = true :: p21 = false fi;
	if :: p22 = true :: p22 = false fi;
	if :: p23 = true :: p23 = false fi;
	if :: p24 = true :: p24 = false fi;
	if :: p25 = true :: p25 = false fi;
	if :: p26 = true :: p26 = false fi;
	if :: p27 = true :: p27 = false fi;
	if :: p28 = true :: p28 = false fi;
	if :: p29 = true :: p29 = false fi;
	if :: p30 = true :: p30 = false fi;
	if :: p31 = true :: p31 = false fi;
	if :: p32 = true :: p32 = false fi;
	if :: p33 = true :: p33 = false fi;
	if :: p34 = true :: p34 = false fi;
	if :: p35 = true :: p35 = false fi;

	result =
	(!p0 || !p1 ||  p2 ||  p3 ||  p4 ||  p5) &&
	(!p0 ||  p1 || !p2 ||  p3 ||  p4 ||  p5) &&
	( p0 || !p1 || !p2 ||  p3 ||  p4 ||  p5) &&
	(!p0 ||  p1 ||  p2 || !p3 ||  p4 ||  p5) &&
	( p0 || !p1 ||  p2 || !p3 ||  p4 ||  p5) &&
	( p0 ||  p1 || !p2 || !p3 ||  p4 ||  p5) &&
	(!p0 || !p1 || !p2 || !p3 ||  p4 ||  p5) &&
	(!p0 ||  p1 ||  p2 ||  p3 || !p4 ||  p5) &&
	( p0 || !p1 ||  p2 ||  p3 || !p4 ||  p5) &&
	( p0 ||  p1 || !p2 ||  p3 || !p4 ||  p5) &&
	(!p0 || !p1 || !p2 ||  p3 || !p4 ||  p5) &&
	( p0 ||  p1 ||  p2 || !p3 || !p4 ||  p5) &&
	(!p0 || !p1 ||  p2 || !p3 || !p4 ||  p5) &&
	(!p0 ||  p1 || !p2 || !p3 || !p4 ||  p5) &&
	( p0 || !p1 || !p2 || !p3 || !p4 ||  p5) &&
	(!p0 ||  p1 ||  p2 ||  p3 ||  p4 || !p5) &&
	( p0 || !p1 ||  p2 ||  p3 ||  p4 || !p5) &&
	( p0 ||  p1 || !p2 ||  p3 ||  p4 || !p5) &&
	(!p0 || !p1 || !p2 ||  p3 ||  p4 || !p5) &&
	( p0 ||  p1 ||  p2 || !p3 ||  p4 || !p5) &&
	(!p0 || !p1 ||  p2 || !p3 ||  p4 || !p5) &&
	(!p0 ||  p1 || !p2 || !p3 ||  p4 || !p5) &&
	( p0 || !p1 || !p2 || !p3 ||  p4 || !p5) &&
	( p0 ||  p1 ||  p2 ||  p3 || !p4 || !p5) &&
	(!p0 || !p1 ||  p2 ||  p3 || !p4 || !p5) &&
	(!p0 ||  p1 || !p2 ||  p3 || !p4 || !p5) &&
	( p0 || !p1 || !p2 ||  p3 || !p4 || !p5) &&
	(!p0 ||  p1 ||  p2 || !p3 || !p4 || !p5) &&
	( p0 || !p1 ||  p2 || !p3 || !p4 || !p5) &&
	( p0 ||  p1 || !p2 || !p3 || !p4 || !p5) &&
	(!p0 || !p1 || !p2 || !p3 || !p4 || !p5) &&
	( p0 ||  p1 ||  p2 ||  p3 ||  p4 ||  p5) &&
	(!p6 ||  p7 ||  p8 ||  p9 ||  p10 ||  p11) &&
	( p6 || !p7 ||  p8 ||  p9 ||  p10 ||  p11) &&
	( p6 ||  p7 || !p8 ||  p9 ||  p10 ||  p11) &&
	(!p6 || !p7 || !p8 ||  p9 ||  p10 ||  p11) &&
	( p6 ||  p7 ||  p8 || !p9 ||  p10 ||  p11) &&
	(!p6 || !p7 ||  p8 || !p9 ||  p10 ||  p11) &&
	(!p6 ||  p7 || !p8 || !p9 ||  p10 ||  p11) &&
	( p6 || !p7 || !p8 || !p9 ||  p10 ||  p11) &&
	( p6 ||  p7 ||  p8 ||  p9 || !p10 ||  p11) &&
	(!p6 || !p7 ||  p8 ||  p9 || !p10 ||  p11) &&
	(!p6 ||  p7 || !p8 ||  p9 || !p10 ||  p11) &&
	( p6 || !p7 || !p8 ||  p9 || !p10 ||  p11) &&
	(!p6 ||  p7 ||  p8 || !p9 || !p10 ||  p11) &&
	( p6 || !p7 ||  p8 || !p9 || !p10 ||  p11) &&
	( p6 ||  p7 || !p8 || !p9 || !p10 ||  p11) &&
	(!p6 || !p7 || !p8 || !p9 || !p10 ||  p11) &&
	( p6 ||  p7 ||  p8 ||  p9 ||  p10 || !p11) &&
	(!p6 || !p7 ||  p8 ||  p9 ||  p10 || !p11) &&
	(!p6 ||  p7 || !p8 ||  p9 ||  p10 || !p11) &&
	( p6 || !p7 || !p8 ||  p9 ||  p10 || !p11) &&
	(!p6 ||  p7 ||  p8 || !p9 ||  p10 || !p11) &&
	( p6 || !p7 ||  p8 || !p9 ||  p10 || !p11) &&
	( p6 ||  p7 || !p8 || !p9 ||  p10 || !p11) &&
	(!p6 || !p7 || !p8 || !p9 ||  p10 || !p11) &&
	(!p6 ||  p7 ||  p8 ||  p9 || !p10 || !p11) &&
	( p6 || !p7 ||  p8 ||  p9 || !p10 || !p11) &&
	( p6 ||  p7 || !p8 ||  p9 || !p10 || !p11) &&
	(!p6 || !p7 || !p8 ||  p9 || !p10 || !p11) &&
	( p6 ||  p7 ||  p8 || !p9 || !p10 || !p11) &&
	(!p6 || !p7 ||  p8 || !p9 || !p10 || !p11) &&
	(!p6 ||  p7 || !p8 || !p9 || !p10 || !p11) &&
	( p6 || !p7 || !p8 || !p9 || !p10 || !p11) &&
	(!p12 ||  p13 ||  p14 ||  p15 ||  p16 ||  p17) &&
	( p12 || !p13 ||  p14 ||  p15 ||  p16 ||  p17) &&
	( p12 ||  p13 || !p14 ||  p15 ||  p16 ||  p17) &&
	(!p12 || !p13 || !p14 ||  p15 ||  p16 ||  p17) &&
	( p12 ||  p13 ||  p14 || !p15 ||  p16 ||  p17) &&
	(!p12 || !p13 ||  p14 || !p15 ||  p16 ||  p17) &&
	(!p12 ||  p13 || !p14 || !p15 ||  p16 ||  p17) &&
	( p12 || !p13 || !p14 || !p15 ||  p16 ||  p17) &&
	( p12 ||  p13 ||  p14 ||  p15 || !p16 ||  p17) &&
	(!p12 || !p13 ||  p14 ||  p15 || !p16 ||  p17) &&
	(!p12 ||  p13 || !p14 ||  p15 || !p16 ||  p17) &&
	( p12 || !p13 || !p14 ||  p15 || !p16 ||  p17) &&
	(!p12 ||  p13 ||  p14 || !p15 || !p16 ||  p17) &&
	( p12 || !p13 ||  p14 || !p15 || !p16 ||  p17) &&
	( p12 ||  p13 || !p14 || !p15 || !p16 ||  p17) &&
	(!p12 || !p13 || !p14 || !p15 || !p16 ||  p17) &&
	( p12 ||  p13 ||  p14 ||  p15 ||  p16 || !p17) &&
	(!p12 || !p13 ||  p14 ||  p15 ||  p16 || !p17) &&
	(!p12 ||  p13 || !p14 ||  p15 ||  p16 || !p17) &&
	( p12 || !p13 || !p14 ||  p15 ||  p16 || !p17) &&
	(!p12 ||  p13 ||  p14 || !p15 ||  p16 || !p17) &&
	( p12 || !p13 ||  p14 || !p15 ||  p16 || !p17) &&
	( p12 ||  p13 || !p14 || !p15 ||  p16 || !p17) &&
	(!p12 || !p13 || !p14 || !p15 ||  p16 || !p17) &&
	(!p12 ||  p13 ||  p14 ||  p15 || !p16 || !p17) &&
	( p12 || !p13 ||  p14 ||  p15 || !p16 || !p17) &&
	( p12 ||  p13 || !p14 ||  p15 || !p16 || !p17) &&
	(!p12 || !p13 || !p14 ||  p15 || !p16 || !p17) &&
	( p12 ||  p13 ||  p14 || !p15 || !p16 || !p17) &&
	(!p12 || !p13 ||  p14 || !p15 || !p16 || !p17) &&
	(!p12 ||  p13 || !p14 || !p15 || !p16 || !p17) &&
	( p12 || !p13 || !p14 || !p15 || !p16 || !p17) &&
	(!p18 ||  p19 ||  p20 ||  p21 ||  p22 ||  p23) &&
	( p18 || !p19 ||  p20 ||  p21 ||  p22 ||  p23) &&
	( p18 ||  p19 || !p20 ||  p21 ||  p22 ||  p23) &&
	(!p18 || !p19 || !p20 ||  p21 ||  p22 ||  p23) &&
	( p18 ||  p19 ||  p20 || !p21 ||  p22 ||  p23) &&
	(!p18 || !p19 ||  p20 || !p21 ||  p22 ||  p23) &&
	(!p18 ||  p19 || !p20 || !p21 ||  p22 ||  p23) &&
	( p18 || !p19 || !p20 || !p21 ||  p22 ||  p23) &&
	( p18 ||  p19 ||  p20 ||  p21 || !p22 ||  p23) &&
	(!p18 || !p19 ||  p20 ||  p21 || !p22 ||  p23) &&
	(!p18 ||  p19 || !p20 ||  p21 || !p22 ||  p23) &&
	( p18 || !p19 || !p20 ||  p21 || !p22 ||  p23) &&
	(!p18 ||  p19 ||  p20 || !p21 || !p22 ||  p23) &&
	( p18 || !p19 ||  p20 || !p21 || !p22 ||  p23) &&
	( p18 ||  p19 || !p20 || !p21 || !p22 ||  p23) &&
	(!p18 || !p19 || !p20 || !p21 || !p22 ||  p23) &&
	( p18 ||  p19 ||  p20 ||  p21 ||  p22 || !p23) &&
	(!p18 || !p19 ||  p20 ||  p21 ||  p22 || !p23) &&
	(!p18 ||  p19 || !p20 ||  p21 ||  p22 || !p23) &&
	( p18 || !p19 || !p20 ||  p21 ||  p22 || !p23) &&
	(!p18 ||  p19 ||  p20 || !p21 ||  p22 || !p23) &&
	( p18 || !p19 ||  p20 || !p21 ||  p22 || !p23) &&
	( p18 ||  p19 || !p20 || !p21 ||  p22 || !p23) &&
	(!p18 || !p19 || !p20 || !p21 ||  p22 || !p23) &&
	(!p18 ||  p19 ||  p20 ||  p21 || !p22 || !p23) &&
	( p18 || !p19 ||  p20 ||  p21 || !p22 || !p23) &&
	( p18 ||  p19 || !p20 ||  p21 || !p22 || !p23) &&
	(!p18 || !p19 || !p20 ||  p21 || !p22 || !p23) &&
	( p18 ||  p19 ||  p20 || !p21 || !p22 || !p23) &&
	(!p18 || !p19 ||  p20 || !p21 || !p22 || !p23) &&
	(!p18 ||  p19 || !p20 || !p21 || !p22 || !p23) &&
	( p18 || !p19 || !p20 || !p21 || !p22 || !p23) &&
	(!p24 ||  p25 ||  p26 ||  p27 ||  p28 ||  p29) &&
	( p24 || !p25 ||  p26 ||  p27 ||  p28 ||  p29) &&
	( p24 ||  p25 || !p26 ||  p27 ||  p28 ||  p29) &&
	(!p24 || !p25 || !p26 ||  p27 ||  p28 ||  p29) &&
	( p24 ||  p25 ||  p26 || !p27 ||  p28 ||  p29) &&
	(!p24 || !p25 ||  p26 || !p27 ||  p28 ||  p29) &&
	(!p24 ||  p25 || !p26 || !p27 ||  p28 ||  p29) &&
	( p24 || !p25 || !p26 || !p27 ||  p28 ||  p29) &&
	( p24 ||  p25 ||  p26 ||  p27 || !p28 ||  p29) &&
	(!p24 || !p25 ||  p26 ||  p27 || !p28 ||  p29) &&
	(!p24 ||  p25 || !p26 ||  p27 || !p28 ||  p29) &&
	( p24 || !p25 || !p26 ||  p27 || !p28 ||  p29) &&
	(!p24 ||  p25 ||  p26 || !p27 || !p28 ||  p29) &&
	( p24 || !p25 ||  p26 || !p27 || !p28 ||  p29) &&
	( p24 ||  p25 || !p26 || !p27 || !p28 ||  p29) &&
	(!p24 || !p25 || !p26 || !p27 || !p28 ||  p29) &&
	( p24 ||  p25 ||  p26 ||  p27 ||  p28 || !p29) &&
	(!p24 || !p25 ||  p26 ||  p27 ||  p28 || !p29) &&
	(!p24 ||  p25 || !p26 ||  p27 ||  p28 || !p29) &&
	( p24 || !p25 || !p26 ||  p27 ||  p28 || !p29) &&
	(!p24 ||  p25 ||  p26 || !p27 ||  p28 || !p29) &&
	( p24 || !p25 ||  p26 || !p27 ||  p28 || !p29) &&
	( p24 ||  p25 || !p26 || !p27 ||  p28 || !p29) &&
	(!p24 || !p25 || !p26 || !p27 ||  p28 || !p29) &&
	(!p24 ||  p25 ||  p26 ||  p27 || !p28 || !p29) &&
	( p24 || !p25 ||  p26 ||  p27 || !p28 || !p29) &&
	( p24 ||  p25 || !p26 ||  p27 || !p28 || !p29) &&
	(!p24 || !p25 || !p26 ||  p27 || !p28 || !p29) &&
	( p24 ||  p25 ||  p26 || !p27 || !p28 || !p29) &&
	(!p24 || !p25 ||  p26 || !p27 || !p28 || !p29) &&
	(!p24 ||  p25 || !p26 || !p27 || !p28 || !p29) &&
	( p24 || !p25 || !p26 || !p27 || !p28 || !p29) &&
	(!p30 ||  p31 ||  p32 ||  p33 ||  p34 ||  p35) &&
	( p30 || !p31 ||  p32 ||  p33 ||  p34 ||  p35) &&
	( p30 ||  p31 || !p32 ||  p33 ||  p34 ||  p35) &&
	(!p30 || !p31 || !p32 ||  p33 ||  p34 ||  p35) &&
	( p30 ||  p31 ||  p32 || !p33 ||  p34 ||  p35) &&
	(!p30 || !p31 ||  p32 || !p33 ||  p34 ||  p35) &&
	(!p30 ||  p31 || !p32 || !p33 ||  p34 ||  p35) &&
	( p30 || !p31 || !p32 || !p33 ||  p34 ||  p35) &&
	( p30 ||  p31 ||  p32 ||  p33 || !p34 ||  p35) &&
	(!p30 || !p31 ||  p32 ||  p33 || !p34 ||  p35) &&
	(!p30 ||  p31 || !p32 ||  p33 || !p34 ||  p35) &&
	( p30 || !p31 || !p32 ||  p33 || !p34 ||  p35) &&
	(!p30 ||  p31 ||  p32 || !p33 || !p34 ||  p35) &&
	( p30 || !p31 ||  p32 || !p33 || !p34 ||  p35) &&
	( p30 ||  p31 || !p32 || !p33 || !p34 ||  p35) &&
	(!p30 || !p31 || !p32 || !p33 || !p34 ||  p35) &&
	( p30 ||  p31 ||  p32 ||  p33 ||  p34 || !p35) &&
	(!p30 || !p31 ||  p32 ||  p33 ||  p34 || !p35) &&
	(!p30 ||  p31 || !p32 ||  p33 ||  p34 || !p35) &&
	( p30 || !p31 || !p32 ||  p33 ||  p34 || !p35) &&
	(!p30 ||  p31 ||  p32 || !p33 ||  p34 || !p35) &&
	( p30 || !p31 ||  p32 || !p33 ||  p34 || !p35) &&
	( p30 ||  p31 || !p32 || !p33 ||  p34 || !p35) &&
	(!p30 || !p31 || !p32 || !p33 ||  p34 || !p35) &&
	(!p30 ||  p31 ||  p32 ||  p33 || !p34 || !p35) &&
	( p30 || !p31 ||  p32 ||  p33 || !p34 || !p35) &&
	( p30 ||  p31 || !p32 ||  p33 || !p34 || !p35) &&
	(!p30 || !p31 || !p32 ||  p33 || !p34 || !p35) &&
	( p30 ||  p31 ||  p32 || !p33 || !p34 || !p35) &&
	(!p30 || !p31 ||  p32 || !p33 || !p34 || !p35) &&
	(!p30 ||  p31 || !p32 || !p33 || !p34 || !p35) &&
	( p30 || !p31 || !p32 || !p33 || !p34 || !p35) &&
	(!p0 ||  p6 ||  p12 ||  p18 ||  p24 ||  p30) &&
	( p0 || !p6 ||  p12 ||  p18 ||  p24 ||  p30) &&
	( p0 ||  p6 || !p12 ||  p18 ||  p24 ||  p30) &&
	(!p0 || !p6 || !p12 ||  p18 ||  p24 ||  p30) &&
	( p0 ||  p6 ||  p12 || !p18 ||  p24 ||  p30) &&
	(!p0 || !p6 ||  p12 || !p18 ||  p24 ||  p30) &&
	(!p0 ||  p6 || !p12 || !p18 ||  p24 ||  p30) &&
	( p0 || !p6 || !p12 || !p18 ||  p24 ||  p30) &&
	( p0 ||  p6 ||  p12 ||  p18 || !p24 ||  p30) &&
	(!p0 || !p6 ||  p12 ||  p18 || !p24 ||  p30) &&
	(!p0 ||  p6 || !p12 ||  p18 || !p24 ||  p30) &&
	( p0 || !p6 || !p12 ||  p18 || !p24 ||  p30) &&
	(!p0 ||  p6 ||  p12 || !p18 || !p24 ||  p30) &&
	( p0 || !p6 ||  p12 || !p18 || !p24 ||  p30) &&
	( p0 ||  p6 || !p12 || !p18 || !p24 ||  p30) &&
	(!p0 || !p6 || !p12 || !p18 || !p24 ||  p30) &&
	( p0 ||  p6 ||  p12 ||  p18 ||  p24 || !p30) &&
	(!p0 || !p6 ||  p12 ||  p18 ||  p24 || !p30) &&
	(!p0 ||  p6 || !p12 ||  p18 ||  p24 || !p30) &&
	( p0 || !p6 || !p12 ||  p18 ||  p24 || !p30) &&
	(!p0 ||  p6 ||  p12 || !p18 ||  p24 || !p30) &&
	( p0 || !p6 ||  p12 || !p18 ||  p24 || !p30) &&
	( p0 ||  p6 || !p12 || !p18 ||  p24 || !p30) &&
	(!p0 || !p6 || !p12 || !p18 ||  p24 || !p30) &&
	(!p0 ||  p6 ||  p12 ||  p18 || !p24 || !p30) &&
	( p0 || !p6 ||  p12 ||  p18 || !p24 || !p30) &&
	( p0 ||  p6 || !p12 ||  p18 || !p24 || !p30) &&
	(!p0 || !p6 || !p12 ||  p18 || !p24 || !p30) &&
	( p0 ||  p6 ||  p12 || !p18 || !p24 || !p30) &&
	(!p0 || !p6 ||  p12 || !p18 || !p24 || !p30) &&
	(!p0 ||  p6 || !p12 || !p18 || !p24 || !p30) &&
	( p0 || !p6 || !p12 || !p18 || !p24 || !p30) &&
	(!p1 ||  p7 ||  p13 ||  p19 ||  p25 ||  p31) &&
	( p1 || !p7 ||  p13 ||  p19 ||  p25 ||  p31) &&
	( p1 ||  p7 || !p13 ||  p19 ||  p25 ||  p31) &&
	(!p1 || !p7 || !p13 ||  p19 ||  p25 ||  p31) &&
	( p1 ||  p7 ||  p13 || !p19 ||  p25 ||  p31) &&
	(!p1 || !p7 ||  p13 || !p19 ||  p25 ||  p31) &&
	(!p1 ||  p7 || !p13 || !p19 ||  p25 ||  p31) &&
	( p1 || !p7 || !p13 || !p19 ||  p25 ||  p31) &&
	( p1 ||  p7 ||  p13 ||  p19 || !p25 ||  p31) &&
	(!p1 || !p7 ||  p13 ||  p19 || !p25 ||  p31) &&
	(!p1 ||  p7 || !p13 ||  p19 || !p25 ||  p31) &&
	( p1 || !p7 || !p13 ||  p19 || !p25 ||  p31) &&
	(!p1 ||  p7 ||  p13 || !p19 || !p25 ||  p31) &&
	( p1 || !p7 ||  p13 || !p19 || !p25 ||  p31) &&
	( p1 ||  p7 || !p13 || !p19 || !p25 ||  p31) &&
	(!p1 || !p7 || !p13 || !p19 || !p25 ||  p31) &&
	( p1 ||  p7 ||  p13 ||  p19 ||  p25 || !p31) &&
	(!p1 || !p7 ||  p13 ||  p19 ||  p25 || !p31) &&
	(!p1 ||  p7 || !p13 ||  p19 ||  p25 || !p31) &&
	( p1 || !p7 || !p13 ||  p19 ||  p25 || !p31) &&
	(!p1 ||  p7 ||  p13 || !p19 ||  p25 || !p31) &&
	( p1 || !p7 ||  p13 || !p19 ||  p25 || !p31) &&
	( p1 ||  p7 || !p13 || !p19 ||  p25 || !p31) &&
	(!p1 || !p7 || !p13 || !p19 ||  p25 || !p31) &&
	(!p1 ||  p7 ||  p13 ||  p19 || !p25 || !p31) &&
	( p1 || !p7 ||  p13 ||  p19 || !p25 || !p31) &&
	( p1 ||  p7 || !p13 ||  p19 || !p25 || !p31) &&
	(!p1 || !p7 || !p13 ||  p19 || !p25 || !p31) &&
	( p1 ||  p7 ||  p13 || !p19 || !p25 || !p31) &&
	(!p1 || !p7 ||  p13 || !p19 || !p25 || !p31) &&
	(!p1 ||  p7 || !p13 || !p19 || !p25 || !p31) &&
	( p1 || !p7 || !p13 || !p19 || !p25 || !p31) &&
	(!p2 ||  p8 ||  p14 ||  p20 ||  p26 ||  p32) &&
	( p2 || !p8 ||  p14 ||  p20 ||  p26 ||  p32) &&
	( p2 ||  p8 || !p14 ||  p20 ||  p26 ||  p32) &&
	(!p2 || !p8 || !p14 ||  p20 ||  p26 ||  p32) &&
	( p2 ||  p8 ||  p14 || !p20 ||  p26 ||  p32) &&
	(!p2 || !p8 ||  p14 || !p20 ||  p26 ||  p32) &&
	(!p2 ||  p8 || !p14 || !p20 ||  p26 ||  p32) &&
	( p2 || !p8 || !p14 || !p20 ||  p26 ||  p32) &&
	( p2 ||  p8 ||  p14 ||  p20 || !p26 ||  p32) &&
	(!p2 || !p8 ||  p14 ||  p20 || !p26 ||  p32) &&
	(!p2 ||  p8 || !p14 ||  p20 || !p26 ||  p32) &&
	( p2 || !p8 || !p14 ||  p20 || !p26 ||  p32) &&
	(!p2 ||  p8 ||  p14 || !p20 || !p26 ||  p32) &&
	( p2 || !p8 ||  p14 || !p20 || !p26 ||  p32) &&
	( p2 ||  p8 || !p14 || !p20 || !p26 ||  p32) &&
	(!p2 || !p8 || !p14 || !p20 || !p26 ||  p32) &&
	( p2 ||  p8 ||  p14 ||  p20 ||  p26 || !p32) &&
	(!p2 || !p8 ||  p14 ||  p20 ||  p26 || !p32) &&
	(!p2 ||  p8 || !p14 ||  p20 ||  p26 || !p32) &&
	( p2 || !p8 || !p14 ||  p20 ||  p26 || !p32) &&
	(!p2 ||  p8 ||  p14 || !p20 ||  p26 || !p32) &&
	( p2 || !p8 ||  p14 || !p20 ||  p26 || !p32) &&
	( p2 ||  p8 || !p14 || !p20 ||  p26 || !p32) &&
	(!p2 || !p8 || !p14 || !p20 ||  p26 || !p32) &&
	(!p2 ||  p8 ||  p14 ||  p20 || !p26 || !p32) &&
	( p2 || !p8 ||  p14 ||  p20 || !p26 || !p32) &&
	( p2 ||  p8 || !p14 ||  p20 || !p26 || !p32) &&
	(!p2 || !p8 || !p14 ||  p20 || !p26 || !p32) &&
	( p2 ||  p8 ||  p14 || !p20 || !p26 || !p32) &&
	(!p2 || !p8 ||  p14 || !p20 || !p26 || !p32) &&
	(!p2 ||  p8 || !p14 || !p20 || !p26 || !p32) &&
	( p2 || !p8 || !p14 || !p20 || !p26 || !p32) &&
	(!p3 ||  p9 ||  p15 ||  p21 ||  p27 ||  p33) &&
	( p3 || !p9 ||  p15 ||  p21 ||  p27 ||  p33) &&
	( p3 ||  p9 || !p15 ||  p21 ||  p27 ||  p33) &&
	(!p3 || !p9 || !p15 ||  p21 ||  p27 ||  p33) &&
	( p3 ||  p9 ||  p15 || !p21 ||  p27 ||  p33) &&
	(!p3 || !p9 ||  p15 || !p21 ||  p27 ||  p33) &&
	(!p3 ||  p9 || !p15 || !p21 ||  p27 ||  p33) &&
	( p3 || !p9 || !p15 || !p21 ||  p27 ||  p33) &&
	( p3 ||  p9 ||  p15 ||  p21 || !p27 ||  p33) &&
	(!p3 || !p9 ||  p15 ||  p21 || !p27 ||  p33) &&
	(!p3 ||  p9 || !p15 ||  p21 || !p27 ||  p33) &&
	( p3 || !p9 || !p15 ||  p21 || !p27 ||  p33) &&
	(!p3 ||  p9 ||  p15 || !p21 || !p27 ||  p33) &&
	( p3 || !p9 ||  p15 || !p21 || !p27 ||  p33) &&
	( p3 ||  p9 || !p15 || !p21 || !p27 ||  p33) &&
	(!p3 || !p9 || !p15 || !p21 || !p27 ||  p33) &&
	( p3 ||  p9 ||  p15 ||  p21 ||  p27 || !p33) &&
	(!p3 || !p9 ||  p15 ||  p21 ||  p27 || !p33) &&
	(!p3 ||  p9 || !p15 ||  p21 ||  p27 || !p33) &&
	( p3 || !p9 || !p15 ||  p21 ||  p27 || !p33) &&
	(!p3 ||  p9 ||  p15 || !p21 ||  p27 || !p33) &&
	( p3 || !p9 ||  p15 || !p21 ||  p27 || !p33) &&
	( p3 ||  p9 || !p15 || !p21 ||  p27 || !p33) &&
	(!p3 || !p9 || !p15 || !p21 ||  p27 || !p33) &&
	(!p3 ||  p9 ||  p15 ||  p21 || !p27 || !p33) &&
	( p3 || !p9 ||  p15 ||  p21 || !p27 || !p33) &&
	( p3 ||  p9 || !p15 ||  p21 || !p27 || !p33) &&
	(!p3 || !p9 || !p15 ||  p21 || !p27 || !p33) &&
	( p3 ||  p9 ||  p15 || !p21 || !p27 || !p33) &&
	(!p3 || !p9 ||  p15 || !p21 || !p27 || !p33) &&
	(!p3 ||  p9 || !p15 || !p21 || !p27 || !p33) &&
	( p3 || !p9 || !p15 || !p21 || !p27 || !p33) &&
	(!p4 ||  p10 ||  p16 ||  p22 ||  p28 ||  p34) &&
	( p4 || !p10 ||  p16 ||  p22 ||  p28 ||  p34) &&
	( p4 ||  p10 || !p16 ||  p22 ||  p28 ||  p34) &&
	(!p4 || !p10 || !p16 ||  p22 ||  p28 ||  p34) &&
	( p4 ||  p10 ||  p16 || !p22 ||  p28 ||  p34) &&
	(!p4 || !p10 ||  p16 || !p22 ||  p28 ||  p34) &&
	(!p4 ||  p10 || !p16 || !p22 ||  p28 ||  p34) &&
	( p4 || !p10 || !p16 || !p22 ||  p28 ||  p34) &&
	( p4 ||  p10 ||  p16 ||  p22 || !p28 ||  p34) &&
	(!p4 || !p10 ||  p16 ||  p22 || !p28 ||  p34) &&
	(!p4 ||  p10 || !p16 ||  p22 || !p28 ||  p34) &&
	( p4 || !p10 || !p16 ||  p22 || !p28 ||  p34) &&
	(!p4 ||  p10 ||  p16 || !p22 || !p28 ||  p34) &&
	( p4 || !p10 ||  p16 || !p22 || !p28 ||  p34) &&
	( p4 ||  p10 || !p16 || !p22 || !p28 ||  p34) &&
	(!p4 || !p10 || !p16 || !p22 || !p28 ||  p34) &&
	( p4 ||  p10 ||  p16 ||  p22 ||  p28 || !p34) &&
	(!p4 || !p10 ||  p16 ||  p22 ||  p28 || !p34) &&
	(!p4 ||  p10 || !p16 ||  p22 ||  p28 || !p34) &&
	( p4 || !p10 || !p16 ||  p22 ||  p28 || !p34) &&
	(!p4 ||  p10 ||  p16 || !p22 ||  p28 || !p34) &&
	( p4 || !p10 ||  p16 || !p22 ||  p28 || !p34) &&
	( p4 ||  p10 || !p16 || !p22 ||  p28 || !p34) &&
	(!p4 || !p10 || !p16 || !p22 ||  p28 || !p34) &&
	(!p4 ||  p10 ||  p16 ||  p22 || !p28 || !p34) &&
	( p4 || !p10 ||  p16 ||  p22 || !p28 || !p34) &&
	( p4 ||  p10 || !p16 ||  p22 || !p28 || !p34) &&
	(!p4 || !p10 || !p16 ||  p22 || !p28 || !p34) &&
	( p4 ||  p10 ||  p16 || !p22 || !p28 || !p34) &&
	(!p4 || !p10 ||  p16 || !p22 || !p28 || !p34) &&
	(!p4 ||  p10 || !p16 || !p22 || !p28 || !p34) &&
	( p4 || !p10 || !p16 || !p22 || !p28 || !p34) &&
	(!p5 ||  p11 ||  p17 ||  p23 ||  p29 ||  p35) &&
	( p5 || !p11 ||  p17 ||  p23 ||  p29 ||  p35) &&
	( p5 ||  p11 || !p17 ||  p23 ||  p29 ||  p35) &&
	(!p5 || !p11 || !p17 ||  p23 ||  p29 ||  p35) &&
	( p5 ||  p11 ||  p17 || !p23 ||  p29 ||  p35) &&
	(!p5 || !p11 ||  p17 || !p23 ||  p29 ||  p35) &&
	(!p5 ||  p11 || !p17 || !p23 ||  p29 ||  p35) &&
	( p5 || !p11 || !p17 || !p23 ||  p29 ||  p35) &&
	( p5 ||  p11 ||  p17 ||  p23 || !p29 ||  p35) &&
	(!p5 || !p11 ||  p17 ||  p23 || !p29 ||  p35) &&
	(!p5 ||  p11 || !p17 ||  p23 || !p29 ||  p35) &&
	( p5 || !p11 || !p17 ||  p23 || !p29 ||  p35) &&
	(!p5 ||  p11 ||  p17 || !p23 || !p29 ||  p35) &&
	( p5 || !p11 ||  p17 || !p23 || !p29 ||  p35) &&
	( p5 ||  p11 || !p17 || !p23 || !p29 ||  p35) &&
	(!p5 || !p11 || !p17 || !p23 || !p29 ||  p35) &&
	( p5 ||  p11 ||  p17 ||  p23 ||  p29 || !p35) &&
	(!p5 || !p11 ||  p17 ||  p23 ||  p29 || !p35) &&
	(!p5 ||  p11 || !p17 ||  p23 ||  p29 || !p35) &&
	( p5 || !p11 || !p17 ||  p23 ||  p29 || !p35) &&
	(!p5 ||  p11 ||  p17 || !p23 ||  p29 || !p35) &&
	( p5 || !p11 ||  p17 || !p23 ||  p29 || !p35) &&
	( p5 ||  p11 || !p17 || !p23 ||  p29 || !p35) &&
	(!p5 || !p11 || !p17 || !p23 ||  p29 || !p35) &&
	(!p5 ||  p11 ||  p17 ||  p23 || !p29 || !p35) &&
	( p5 || !p11 ||  p17 ||  p23 || !p29 || !p35) &&
	( p5 ||  p11 || !p17 ||  p23 || !p29 || !p35) &&
	(!p5 || !p11 || !p17 ||  p23 || !p29 || !p35) &&
	( p5 ||  p11 ||  p17 || !p23 || !p29 || !p35) &&
	(!p5 || !p11 ||  p17 || !p23 || !p29 || !p35) &&
	(!p5 ||  p11 || !p17 || !p23 || !p29 || !p35) &&
	( p5 || !p11 || !p17 || !p23 || !p29 || !p35) &&
	true;

	printf("p0 p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 p11 p12 p13 p14 p15 p16 p17 p18 p19 p20 p21 p22 p23 p24 p25 p26 p27 p28 p29 p30 p31 p32 p33 p34 p35 \n");
	printf(" %d  %d  %d  %d  %d  %d  %d  %d  %d  %d  %d  %d  %d  %d  %d  %d  %d  %d  %d  %d  %d  %d  %d  %d  %d  %d  %d  %d  %d  %d  %d  %d  %d  %d  %d  %d  \n", p0, p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p20, p21, p22, p23, p24, p25, p26, p27, p28, p29, p30, p31, p32, p33, p34, p35);
	printf("Result = %d\n", result);
	assert(!result);
}
